Skip to content

Add missing features#473

Merged
marcoeilers merged 14 commits into
masterfrom
meilers_general_perm_forperm
Feb 2, 2024
Merged

Add missing features#473
marcoeilers merged 14 commits into
masterfrom
meilers_general_perm_forperm

Conversation

@marcoeilers

@marcoeilers marcoeilers commented Oct 28, 2023 •
edited
Loading

Copy link
Copy Markdown
Contributor

@marcoeilers marcoeilers marked this pull request as ready for review January 21, 2024 20:18
@marcoeilers

marcoeilers commented Jan 21, 2024

Copy link
Copy Markdown
Contributor Author
  • forperm is often incomplete, but this is due to triggering. I don't know what better triggers one could choose than { Mask[r, f] } and { Heap[r, f] }, so I don't think we can do anything about that.
  • Resource triggers are also often incomplete. The trigger { x.f } is currently translated as { Heap[x, f] }, so it does not trigger at all on mask accesses. That seems bad to me and would be easy to fix.

gauravpartha
gauravpartha previously requested changes Feb 1, 2024
View reviewed changes

@gauravpartha gauravpartha left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the changes. I just added some minor comments, but looks good to me otherwise.

Comment thread src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala Outdated
Comment thread src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala Outdated
Comment thread src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala
Comment thread src/main/scala/viper/carbon/modules/WandModule.scala Outdated
Comment thread src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala Outdated
Comment thread src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala Outdated
@marcoeilers marcoeilers dismissed gauravpartha’s stale review February 2, 2024 13:26

Addressed all comments

@marcoeilers marcoeilers merged commit 28e12c0 into master Feb 2, 2024
@marcoeilers marcoeilers deleted the meilers_general_perm_forperm branch February 2, 2024 13:26
@marcoeilers marcoeilers mentioned this pull request Feb 2, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@gauravpartha gauravpartha gauravpartha left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@marcoeilers @gauravpartha
⚡